/*
	アドレス帳にアドレスを追加する操作を登録する
*/

module tour/addressBook2

// 名前
sig Name {}

// アドレス
sig Addr {}

// アドレス帳
sig Book { 
	addr: Name -> lone Addr
}

// アドレス帳にアドレスを追加する操作
pred add (b, b': Book, n: Name, a: Addr) {
	b'.addr = b.addr + n -> a
}
//run add for 3 but 2 Book
pred showAdd (b, b': Book, n: Name, a: Addr) {
	add [b, b', n, a]

	// 追加後のアドレス１つに対応する名称が複数存在するパターンがあるか確認
	#Name.(b'.addr) > 1
}
run showAdd for 3 but 2 Book

// 表示
pred show (b:Book) {
	// アドレス帳に1つ以上のアドレスが存在できることを確認。
	#b.addr > 1
	
	// 1つの名称に紐づくアドレスが指定した数存在できるか確認。
	// some n: Name | #n.(b.addr) < 1

	// アドレス帳のアドレスと紐づく名称が複数あるパターンを確認。
	#Name.(b.addr) > 1

}
run show for 5 but 1 Book
